$\forall$$T$:Type, $A$:($T$$\rightarrow$Prop). detach\_fun($T$;$A$) $\in$ Type